Arrazoiketa automatiko

Arrazoiketa automatikoa (edo arrazoibide automatikoa) informatikaren eremu bat ezagutzaren errepresentazioa eta arrazoibideak) eta metalogika eremuak bere barruan darabiltzana, eta arrazoitzeko moduak ulertzeko hainbat alderdi lantzen dituena. Arrazoibide automatizatuaren azterketak arrazoitzea ahalbidetzen duten programa informatikoak sortzen laguntzen du, erabat edo ia erabat automatikoki. Arrazoibide automatizatuak adimen artifizialaren azpi-eremutzat jotzen diren arren, informatika teorikoarekin eta filosofiarekin ere baditu loturak.

Arrazoibide automatizatuen azpieremu garatuenak teoremen frogapen automatikoa (eta hain automatikoa ez den baina pragmatikoa den teoremen frogapen interaktiboa azpieremua) eta egiaztapen automatizatua (hipotesi finkoen pean arrazoibide zuzen bermatu gisa ikusten dena).  Analogia bidez Indukzio eta abdukzioa erabiliz ere lan handia egin da arrazoibidean. ^[1]

Beste gai garrantzitsuen artean ziurgabetasunaren arrazoibidea eta arrazonamendu ez monotonikoa dira aipagarri. Ziurgabetasunaren eremuko zati garrantzitsu bat argumentazioarena da, non gutxieneko eta koherentziazko muga gehiago aplikatzen diren dedukzio automatizatu estandarragoaren gainean. John Pollock-en OSCAR sistema^[2] teorema-frogapen automatiko bat baino zehatzagoa den argumentazio-sistema automatizatuaren adibidea da.

Arrazoibide automatizatuaren tresna eta teknika batzuk dira honako hauek: logika eta kalkulu klasikoak, logika lausoa, inferentzia bayesiarra, entropia maximoa duten arrazoibideak eta hain formalak ez diren ad hoc teknikak.

1. ↑ Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997.
2. ↑ John L. Pollock